fetch takeuc.ax;
cancel 1;
fetch takeuc.cmd;
∀e LESS4 x y;
taut y<x 4 5 6;
assume y≤z;
∀e LESS1 y;
∀e LESS3 pred y y z;
∀e LESS4 pred y y;
taut pred y ≤ z 8:11;
rewrite tak1(x,y,z)=tak0(x,y,z) by LOGICTREE∪{TAK0,TAK1,4,7,8,12};
ASSUME pred x ≤ y;
REWRITE 13 BY LOGICTREE∪{8,14};
⊃I 14 15;
ASSUME ¬(pred x ≤ y);
REWRITE 13 BY LOGICTREE ∪ {8,17,LESS4};
⊃I 17 18;
TAUT 19:#2 16 19;
ASSUME ¬(y≤z);
∀e LESS2 y z;
∀e LESS4 y z;
taut z<y 21:23;
∀e LESS1 z;
∀e LESS3 pred z z y;
∀e LESS4 pred z z;
∀e LESS4 pred z y;
taut pred z ≤ y 24:↑;